Section: New Software and Platforms

miTLS

Participants : Karthikeyan Bhargavan [correspondant] , Cedric Fournet [Microsoft Research] , Markulf Kohlweiss [Microsoft Research] , Antoine Delignat-Lavaud [Microsoft Research] , Nikhil Swamy [Microsoft Research] , Santiago Zanella-Béguelin [Microsoft Research] , Jean Karim Zinzindohoué, Benjamin Beurdouche, Alfredo Pironti.

miTLS is a verified reference implementation of the TLS security protocol in F#, a dialect of OCaml for the .NET platform. It supports SSL version 3.0 and TLS versions 1.0-1.2 and interoperates with mainstream web browsers and servers. miTLS has been verified for functional correctness and cryptographic security using the refinement typechecker F7.

Papers describing the miTLS library was published at IEEE S&P 2013, CRYPTO 2014, and IEEE S&P Journal 2016. miTLS is now being developed on GitHub with dozens of contributors and regular updates. The miTLS team was awarded the Levchin prize for contributions to Real-World Cryptography in 2016. The software and associated research materials are available from http://mitls.org.